0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 87 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 8 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 55 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 PiDP
↳9 UsableRulesProof (⇔, 0 ms)
↳10 PiDP
↳11 PiDPToQDPProof (⇒, 36 ms)
↳12 QDP
↳13 QDPSizeChangeProof (⇔, 0 ms)
↳14 YES
pA_in_ggga(T30, s(T32), s(T31), T34) → U1_ggga(T30, T32, T31, T34, pA_in_ggga(T30, T32, T31, T34))
pA_in_ggga(T55, T57, s(s(T56)), T59) → U2_ggga(T55, T57, T56, T59, pA_in_ggga(T57, T56, T55, T59))
pA_in_ggga(T76, T78, s(T77), T76) → pA_out_ggga(T76, T78, s(T77), T76)
pA_in_ggga(T95, s(T96), s(T97), T99) → U3_ggga(T95, T96, T97, T99, pA_in_ggga(s(T97), T96, T95, T99))
pA_in_ggga(s(T140), s(T139), T138, T142) → U4_ggga(T140, T139, T138, T142, pA_in_ggga(T138, T140, T139, T142))
pA_in_ggga(T165, s(s(T164)), T163, T167) → U5_ggga(T165, T164, T163, T167, pA_in_ggga(T165, T164, T163, T167))
pA_in_ggga(T190, s(T189), T188, T188) → pA_out_ggga(T190, s(T189), T188, T188)
pA_in_ggga(T197, s(T198), T199, T197) → pA_out_ggga(T197, s(T198), T199, T197)
pA_in_ggga(T203, T204, T205, T203) → pA_out_ggga(T203, T204, T205, T203)
U5_ggga(T165, T164, T163, T167, pA_out_ggga(T165, T164, T163, T167)) → pA_out_ggga(T165, s(s(T164)), T163, T167)
U4_ggga(T140, T139, T138, T142, pA_out_ggga(T138, T140, T139, T142)) → pA_out_ggga(s(T140), s(T139), T138, T142)
U3_ggga(T95, T96, T97, T99, pA_out_ggga(s(T97), T96, T95, T99)) → pA_out_ggga(T95, s(T96), s(T97), T99)
U2_ggga(T55, T57, T56, T59, pA_out_ggga(T57, T56, T55, T59)) → pA_out_ggga(T55, T57, s(s(T56)), T59)
U1_ggga(T30, T32, T31, T34, pA_out_ggga(T30, T32, T31, T34)) → pA_out_ggga(T30, s(T32), s(T31), T34)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
pA_in_ggga(T30, s(T32), s(T31), T34) → U1_ggga(T30, T32, T31, T34, pA_in_ggga(T30, T32, T31, T34))
pA_in_ggga(T55, T57, s(s(T56)), T59) → U2_ggga(T55, T57, T56, T59, pA_in_ggga(T57, T56, T55, T59))
pA_in_ggga(T76, T78, s(T77), T76) → pA_out_ggga(T76, T78, s(T77), T76)
pA_in_ggga(T95, s(T96), s(T97), T99) → U3_ggga(T95, T96, T97, T99, pA_in_ggga(s(T97), T96, T95, T99))
pA_in_ggga(s(T140), s(T139), T138, T142) → U4_ggga(T140, T139, T138, T142, pA_in_ggga(T138, T140, T139, T142))
pA_in_ggga(T165, s(s(T164)), T163, T167) → U5_ggga(T165, T164, T163, T167, pA_in_ggga(T165, T164, T163, T167))
pA_in_ggga(T190, s(T189), T188, T188) → pA_out_ggga(T190, s(T189), T188, T188)
pA_in_ggga(T197, s(T198), T199, T197) → pA_out_ggga(T197, s(T198), T199, T197)
pA_in_ggga(T203, T204, T205, T203) → pA_out_ggga(T203, T204, T205, T203)
U5_ggga(T165, T164, T163, T167, pA_out_ggga(T165, T164, T163, T167)) → pA_out_ggga(T165, s(s(T164)), T163, T167)
U4_ggga(T140, T139, T138, T142, pA_out_ggga(T138, T140, T139, T142)) → pA_out_ggga(s(T140), s(T139), T138, T142)
U3_ggga(T95, T96, T97, T99, pA_out_ggga(s(T97), T96, T95, T99)) → pA_out_ggga(T95, s(T96), s(T97), T99)
U2_ggga(T55, T57, T56, T59, pA_out_ggga(T57, T56, T55, T59)) → pA_out_ggga(T55, T57, s(s(T56)), T59)
U1_ggga(T30, T32, T31, T34, pA_out_ggga(T30, T32, T31, T34)) → pA_out_ggga(T30, s(T32), s(T31), T34)
PA_IN_GGGA(T30, s(T32), s(T31), T34) → U1_GGGA(T30, T32, T31, T34, pA_in_ggga(T30, T32, T31, T34))
PA_IN_GGGA(T30, s(T32), s(T31), T34) → PA_IN_GGGA(T30, T32, T31, T34)
PA_IN_GGGA(T55, T57, s(s(T56)), T59) → U2_GGGA(T55, T57, T56, T59, pA_in_ggga(T57, T56, T55, T59))
PA_IN_GGGA(T55, T57, s(s(T56)), T59) → PA_IN_GGGA(T57, T56, T55, T59)
PA_IN_GGGA(T95, s(T96), s(T97), T99) → U3_GGGA(T95, T96, T97, T99, pA_in_ggga(s(T97), T96, T95, T99))
PA_IN_GGGA(T95, s(T96), s(T97), T99) → PA_IN_GGGA(s(T97), T96, T95, T99)
PA_IN_GGGA(s(T140), s(T139), T138, T142) → U4_GGGA(T140, T139, T138, T142, pA_in_ggga(T138, T140, T139, T142))
PA_IN_GGGA(s(T140), s(T139), T138, T142) → PA_IN_GGGA(T138, T140, T139, T142)
PA_IN_GGGA(T165, s(s(T164)), T163, T167) → U5_GGGA(T165, T164, T163, T167, pA_in_ggga(T165, T164, T163, T167))
PA_IN_GGGA(T165, s(s(T164)), T163, T167) → PA_IN_GGGA(T165, T164, T163, T167)
pA_in_ggga(T30, s(T32), s(T31), T34) → U1_ggga(T30, T32, T31, T34, pA_in_ggga(T30, T32, T31, T34))
pA_in_ggga(T55, T57, s(s(T56)), T59) → U2_ggga(T55, T57, T56, T59, pA_in_ggga(T57, T56, T55, T59))
pA_in_ggga(T76, T78, s(T77), T76) → pA_out_ggga(T76, T78, s(T77), T76)
pA_in_ggga(T95, s(T96), s(T97), T99) → U3_ggga(T95, T96, T97, T99, pA_in_ggga(s(T97), T96, T95, T99))
pA_in_ggga(s(T140), s(T139), T138, T142) → U4_ggga(T140, T139, T138, T142, pA_in_ggga(T138, T140, T139, T142))
pA_in_ggga(T165, s(s(T164)), T163, T167) → U5_ggga(T165, T164, T163, T167, pA_in_ggga(T165, T164, T163, T167))
pA_in_ggga(T190, s(T189), T188, T188) → pA_out_ggga(T190, s(T189), T188, T188)
pA_in_ggga(T197, s(T198), T199, T197) → pA_out_ggga(T197, s(T198), T199, T197)
pA_in_ggga(T203, T204, T205, T203) → pA_out_ggga(T203, T204, T205, T203)
U5_ggga(T165, T164, T163, T167, pA_out_ggga(T165, T164, T163, T167)) → pA_out_ggga(T165, s(s(T164)), T163, T167)
U4_ggga(T140, T139, T138, T142, pA_out_ggga(T138, T140, T139, T142)) → pA_out_ggga(s(T140), s(T139), T138, T142)
U3_ggga(T95, T96, T97, T99, pA_out_ggga(s(T97), T96, T95, T99)) → pA_out_ggga(T95, s(T96), s(T97), T99)
U2_ggga(T55, T57, T56, T59, pA_out_ggga(T57, T56, T55, T59)) → pA_out_ggga(T55, T57, s(s(T56)), T59)
U1_ggga(T30, T32, T31, T34, pA_out_ggga(T30, T32, T31, T34)) → pA_out_ggga(T30, s(T32), s(T31), T34)
PA_IN_GGGA(T30, s(T32), s(T31), T34) → U1_GGGA(T30, T32, T31, T34, pA_in_ggga(T30, T32, T31, T34))
PA_IN_GGGA(T30, s(T32), s(T31), T34) → PA_IN_GGGA(T30, T32, T31, T34)
PA_IN_GGGA(T55, T57, s(s(T56)), T59) → U2_GGGA(T55, T57, T56, T59, pA_in_ggga(T57, T56, T55, T59))
PA_IN_GGGA(T55, T57, s(s(T56)), T59) → PA_IN_GGGA(T57, T56, T55, T59)
PA_IN_GGGA(T95, s(T96), s(T97), T99) → U3_GGGA(T95, T96, T97, T99, pA_in_ggga(s(T97), T96, T95, T99))
PA_IN_GGGA(T95, s(T96), s(T97), T99) → PA_IN_GGGA(s(T97), T96, T95, T99)
PA_IN_GGGA(s(T140), s(T139), T138, T142) → U4_GGGA(T140, T139, T138, T142, pA_in_ggga(T138, T140, T139, T142))
PA_IN_GGGA(s(T140), s(T139), T138, T142) → PA_IN_GGGA(T138, T140, T139, T142)
PA_IN_GGGA(T165, s(s(T164)), T163, T167) → U5_GGGA(T165, T164, T163, T167, pA_in_ggga(T165, T164, T163, T167))
PA_IN_GGGA(T165, s(s(T164)), T163, T167) → PA_IN_GGGA(T165, T164, T163, T167)
pA_in_ggga(T30, s(T32), s(T31), T34) → U1_ggga(T30, T32, T31, T34, pA_in_ggga(T30, T32, T31, T34))
pA_in_ggga(T55, T57, s(s(T56)), T59) → U2_ggga(T55, T57, T56, T59, pA_in_ggga(T57, T56, T55, T59))
pA_in_ggga(T76, T78, s(T77), T76) → pA_out_ggga(T76, T78, s(T77), T76)
pA_in_ggga(T95, s(T96), s(T97), T99) → U3_ggga(T95, T96, T97, T99, pA_in_ggga(s(T97), T96, T95, T99))
pA_in_ggga(s(T140), s(T139), T138, T142) → U4_ggga(T140, T139, T138, T142, pA_in_ggga(T138, T140, T139, T142))
pA_in_ggga(T165, s(s(T164)), T163, T167) → U5_ggga(T165, T164, T163, T167, pA_in_ggga(T165, T164, T163, T167))
pA_in_ggga(T190, s(T189), T188, T188) → pA_out_ggga(T190, s(T189), T188, T188)
pA_in_ggga(T197, s(T198), T199, T197) → pA_out_ggga(T197, s(T198), T199, T197)
pA_in_ggga(T203, T204, T205, T203) → pA_out_ggga(T203, T204, T205, T203)
U5_ggga(T165, T164, T163, T167, pA_out_ggga(T165, T164, T163, T167)) → pA_out_ggga(T165, s(s(T164)), T163, T167)
U4_ggga(T140, T139, T138, T142, pA_out_ggga(T138, T140, T139, T142)) → pA_out_ggga(s(T140), s(T139), T138, T142)
U3_ggga(T95, T96, T97, T99, pA_out_ggga(s(T97), T96, T95, T99)) → pA_out_ggga(T95, s(T96), s(T97), T99)
U2_ggga(T55, T57, T56, T59, pA_out_ggga(T57, T56, T55, T59)) → pA_out_ggga(T55, T57, s(s(T56)), T59)
U1_ggga(T30, T32, T31, T34, pA_out_ggga(T30, T32, T31, T34)) → pA_out_ggga(T30, s(T32), s(T31), T34)
PA_IN_GGGA(T55, T57, s(s(T56)), T59) → PA_IN_GGGA(T57, T56, T55, T59)
PA_IN_GGGA(T30, s(T32), s(T31), T34) → PA_IN_GGGA(T30, T32, T31, T34)
PA_IN_GGGA(T95, s(T96), s(T97), T99) → PA_IN_GGGA(s(T97), T96, T95, T99)
PA_IN_GGGA(s(T140), s(T139), T138, T142) → PA_IN_GGGA(T138, T140, T139, T142)
PA_IN_GGGA(T165, s(s(T164)), T163, T167) → PA_IN_GGGA(T165, T164, T163, T167)
pA_in_ggga(T30, s(T32), s(T31), T34) → U1_ggga(T30, T32, T31, T34, pA_in_ggga(T30, T32, T31, T34))
pA_in_ggga(T55, T57, s(s(T56)), T59) → U2_ggga(T55, T57, T56, T59, pA_in_ggga(T57, T56, T55, T59))
pA_in_ggga(T76, T78, s(T77), T76) → pA_out_ggga(T76, T78, s(T77), T76)
pA_in_ggga(T95, s(T96), s(T97), T99) → U3_ggga(T95, T96, T97, T99, pA_in_ggga(s(T97), T96, T95, T99))
pA_in_ggga(s(T140), s(T139), T138, T142) → U4_ggga(T140, T139, T138, T142, pA_in_ggga(T138, T140, T139, T142))
pA_in_ggga(T165, s(s(T164)), T163, T167) → U5_ggga(T165, T164, T163, T167, pA_in_ggga(T165, T164, T163, T167))
pA_in_ggga(T190, s(T189), T188, T188) → pA_out_ggga(T190, s(T189), T188, T188)
pA_in_ggga(T197, s(T198), T199, T197) → pA_out_ggga(T197, s(T198), T199, T197)
pA_in_ggga(T203, T204, T205, T203) → pA_out_ggga(T203, T204, T205, T203)
U5_ggga(T165, T164, T163, T167, pA_out_ggga(T165, T164, T163, T167)) → pA_out_ggga(T165, s(s(T164)), T163, T167)
U4_ggga(T140, T139, T138, T142, pA_out_ggga(T138, T140, T139, T142)) → pA_out_ggga(s(T140), s(T139), T138, T142)
U3_ggga(T95, T96, T97, T99, pA_out_ggga(s(T97), T96, T95, T99)) → pA_out_ggga(T95, s(T96), s(T97), T99)
U2_ggga(T55, T57, T56, T59, pA_out_ggga(T57, T56, T55, T59)) → pA_out_ggga(T55, T57, s(s(T56)), T59)
U1_ggga(T30, T32, T31, T34, pA_out_ggga(T30, T32, T31, T34)) → pA_out_ggga(T30, s(T32), s(T31), T34)
PA_IN_GGGA(T55, T57, s(s(T56)), T59) → PA_IN_GGGA(T57, T56, T55, T59)
PA_IN_GGGA(T30, s(T32), s(T31), T34) → PA_IN_GGGA(T30, T32, T31, T34)
PA_IN_GGGA(T95, s(T96), s(T97), T99) → PA_IN_GGGA(s(T97), T96, T95, T99)
PA_IN_GGGA(s(T140), s(T139), T138, T142) → PA_IN_GGGA(T138, T140, T139, T142)
PA_IN_GGGA(T165, s(s(T164)), T163, T167) → PA_IN_GGGA(T165, T164, T163, T167)
PA_IN_GGGA(T55, T57, s(s(T56))) → PA_IN_GGGA(T57, T56, T55)
PA_IN_GGGA(T30, s(T32), s(T31)) → PA_IN_GGGA(T30, T32, T31)
PA_IN_GGGA(T95, s(T96), s(T97)) → PA_IN_GGGA(s(T97), T96, T95)
PA_IN_GGGA(s(T140), s(T139), T138) → PA_IN_GGGA(T138, T140, T139)
PA_IN_GGGA(T165, s(s(T164)), T163) → PA_IN_GGGA(T165, T164, T163)
From the DPs we obtained the following set of size-change graphs: